(state when $e$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$1of(when{-}after($e$;es\_info(${\it es}$);es{-}pred?(${\it es}$);es\_init(${\it es}$);es{-}Trans(${\it es}$);es\_val(${\it es}$)))